Section: Dissemination

Industrial Dissemination

• Alt-Ergo is now used in the Spark Pro toolset, developed by Altran-Praxis, for the engineering of high-assurance software. Alt-Ergo can be used by customers as an alternate prover for automatically proving verification conditions.

• As part of the qualification process of Alt-Ergo with Airbus industry (DO-178B), the technical documents (functional specifications and benchmark suite) have been accepted by Airbus. These documents will be submitted by Airbus to the certification authorities in 2012.

• S. Conchon has started a collaboration with S. Krstic and A. Goel (Intel Strategic Cad Labs in Hillsboro, OR, USA) that aims in the development of an SMT-based model checker. With A. Mebsout and F. Zaidi (ForTesSe, LRI), they implement the Cubicle model checker which uses the Alt-Ergo theorem prover to discharge its proof obligations.

• The Adacore company (Paris) implements a new tool GnatProve which aims at formal verification of Ada programs. They translate annotated Ada code into the Why3 intermediate language and then use the Why3 system to generate proof obligations and discharge them with available back-end provers.

• J.-C. Filliâtre and C. Marché have started a collaboration with D. Mentré at Mitsubishi Electric R&D Centre Europe (Rennes), about the use of the Why3 environment and its back-end provers as an alternative to the built-in prover of Atelier B.